($e$ sends on $l$ with tag ${\it tg}$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$${\it e'}$:es{-}E(${\it es}$). ((es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$)) c$\wedge$ (es{-}sender(${\it es}$; ${\it e'}$) = $e$))